The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isList(nil)) → c5(MARK(tt))
ACTIVE(isList(__(z0, z1))) → c6(MARK(and(isList(z0), isList(z1))), AND(isList(z0), isList(z1)), ISLIST(z0), ISLIST(z1))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
ACTIVE(isPal(nil)) → c13(MARK(tt))
ACTIVE(isQid(a)) → c14(MARK(tt))
ACTIVE(isQid(e)) → c15(MARK(tt))
ACTIVE(isQid(i)) → c16(MARK(tt))
ACTIVE(isQid(o)) → c17(MARK(tt))
ACTIVE(isQid(u)) → c18(MARK(tt))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(nil) → c20(ACTIVE(nil))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(tt) → c22(ACTIVE(tt))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
MARK(a) → c28(ACTIVE(a))
MARK(e) → c29(ACTIVE(e))
MARK(i) → c30(ACTIVE(i))
MARK(o) → c31(ACTIVE(o))
MARK(u) → c32(ACTIVE(u))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isList(nil)) → c5(MARK(tt))
ACTIVE(isList(__(z0, z1))) → c6(MARK(and(isList(z0), isList(z1))), AND(isList(z0), isList(z1)), ISLIST(z0), ISLIST(z1))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
ACTIVE(isPal(nil)) → c13(MARK(tt))
ACTIVE(isQid(a)) → c14(MARK(tt))
ACTIVE(isQid(e)) → c15(MARK(tt))
ACTIVE(isQid(i)) → c16(MARK(tt))
ACTIVE(isQid(o)) → c17(MARK(tt))
ACTIVE(isQid(u)) → c18(MARK(tt))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(nil) → c20(ACTIVE(nil))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(tt) → c22(ACTIVE(tt))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
MARK(a) → c28(ACTIVE(a))
MARK(e) → c29(ACTIVE(e))
MARK(i) → c30(ACTIVE(i))
MARK(o) → c31(ACTIVE(o))
MARK(u) → c32(ACTIVE(u))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 14 trailing nodes:

ACTIVE(isQid(u)) → c18(MARK(tt))
MARK(nil) → c20(ACTIVE(nil))
ACTIVE(isQid(o)) → c17(MARK(tt))
ACTIVE(isQid(i)) → c16(MARK(tt))
MARK(e) → c29(ACTIVE(e))
MARK(o) → c31(ACTIVE(o))
ACTIVE(isQid(e)) → c15(MARK(tt))
ACTIVE(isQid(a)) → c14(MARK(tt))
ACTIVE(isPal(nil)) → c13(MARK(tt))
MARK(a) → c28(ACTIVE(a))
MARK(i) → c30(ACTIVE(i))
MARK(tt) → c22(ACTIVE(tt))
ACTIVE(isList(nil)) → c5(MARK(tt))
MARK(u) → c32(ACTIVE(u))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isList(__(z0, z1))) → c6(MARK(and(isList(z0), isList(z1))), AND(isList(z0), isList(z1)), ISLIST(z0), ISLIST(z1))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isList(__(z0, z1))) → c6(MARK(and(isList(z0), isList(z1))), AND(isList(z0), isList(z1)), ISLIST(z0), ISLIST(z1))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c6, c7, c8, c9, c10, c11, c12, c19, c21, c23, c24, c25, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(isList(__(z0, z1))) → c6(MARK(and(isList(z0), isList(z1))), AND(isList(z0), isList(z1)), ISLIST(z0), ISLIST(z1)) by

ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c19, c21, c23, c24, c25, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c6

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1)) by

ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c7, c9, c10, c11, c12, c19, c21, c23, c24, c25, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c6, c8

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1)) by

ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c7, c10, c11, c12, c19, c21, c23, c24, c25, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c6, c8, c9

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1)) by

ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c7, c10, c12, c19, c21, c23, c24, c25, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c6, c8, c9, c11

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1)) by

MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))
MARK(__(x0, x1)) → c19

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))
MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))
MARK(__(x0, x1)) → c19

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))
MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))
MARK(__(x0, x1)) → c19

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c7, c10, c12, c21, c23, c24, c25, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c6, c8, c9, c11, c19, c19

(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(__(x0, x1)) → c19

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))
MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))
MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c7, c10, c12, c21, c23, c24, c25, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c6, c8, c9, c11, c19

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0)) by

MARK(and(z0, z1)) → c21(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(__(z0, z1), x1)) → c21(ACTIVE(and(active(__(mark(z0), mark(z1))), x1)), AND(mark(__(z0, z1)), x1), MARK(__(z0, z1)))
MARK(and(nil, x1)) → c21(ACTIVE(and(active(nil), x1)), AND(mark(nil), x1), MARK(nil))
MARK(and(and(z0, z1), x1)) → c21(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c21(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(isList(z0), x1)) → c21(ACTIVE(and(active(isList(z0)), x1)), AND(mark(isList(z0)), x1), MARK(isList(z0)))
MARK(and(isNeList(z0), x1)) → c21(ACTIVE(and(active(isNeList(z0)), x1)), AND(mark(isNeList(z0)), x1), MARK(isNeList(z0)))
MARK(and(isQid(z0), x1)) → c21(ACTIVE(and(active(isQid(z0)), x1)), AND(mark(isQid(z0)), x1), MARK(isQid(z0)))
MARK(and(isNePal(z0), x1)) → c21(ACTIVE(and(active(isNePal(z0)), x1)), AND(mark(isNePal(z0)), x1), MARK(isNePal(z0)))
MARK(and(isPal(z0), x1)) → c21(ACTIVE(and(active(isPal(z0)), x1)), AND(mark(isPal(z0)), x1), MARK(isPal(z0)))
MARK(and(a, x1)) → c21(ACTIVE(and(active(a), x1)), AND(mark(a), x1), MARK(a))
MARK(and(e, x1)) → c21(ACTIVE(and(active(e), x1)), AND(mark(e), x1), MARK(e))
MARK(and(i, x1)) → c21(ACTIVE(and(active(i), x1)), AND(mark(i), x1), MARK(i))
MARK(and(o, x1)) → c21(ACTIVE(and(active(o), x1)), AND(mark(o), x1), MARK(o))
MARK(and(u, x1)) → c21(ACTIVE(and(active(u), x1)), AND(mark(u), x1), MARK(u))
MARK(and(x0, x1)) → c21(AND(mark(x0), x1))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))
MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))
MARK(and(z0, z1)) → c21(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(__(z0, z1), x1)) → c21(ACTIVE(and(active(__(mark(z0), mark(z1))), x1)), AND(mark(__(z0, z1)), x1), MARK(__(z0, z1)))
MARK(and(nil, x1)) → c21(ACTIVE(and(active(nil), x1)), AND(mark(nil), x1), MARK(nil))
MARK(and(and(z0, z1), x1)) → c21(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c21(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(isList(z0), x1)) → c21(ACTIVE(and(active(isList(z0)), x1)), AND(mark(isList(z0)), x1), MARK(isList(z0)))
MARK(and(isNeList(z0), x1)) → c21(ACTIVE(and(active(isNeList(z0)), x1)), AND(mark(isNeList(z0)), x1), MARK(isNeList(z0)))
MARK(and(isQid(z0), x1)) → c21(ACTIVE(and(active(isQid(z0)), x1)), AND(mark(isQid(z0)), x1), MARK(isQid(z0)))
MARK(and(isNePal(z0), x1)) → c21(ACTIVE(and(active(isNePal(z0)), x1)), AND(mark(isNePal(z0)), x1), MARK(isNePal(z0)))
MARK(and(isPal(z0), x1)) → c21(ACTIVE(and(active(isPal(z0)), x1)), AND(mark(isPal(z0)), x1), MARK(isPal(z0)))
MARK(and(a, x1)) → c21(ACTIVE(and(active(a), x1)), AND(mark(a), x1), MARK(a))
MARK(and(e, x1)) → c21(ACTIVE(and(active(e), x1)), AND(mark(e), x1), MARK(e))
MARK(and(i, x1)) → c21(ACTIVE(and(active(i), x1)), AND(mark(i), x1), MARK(i))
MARK(and(o, x1)) → c21(ACTIVE(and(active(o), x1)), AND(mark(o), x1), MARK(o))
MARK(and(u, x1)) → c21(ACTIVE(and(active(u), x1)), AND(mark(u), x1), MARK(u))
MARK(and(x0, x1)) → c21(AND(mark(x0), x1))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))
MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))
MARK(and(z0, z1)) → c21(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(__(z0, z1), x1)) → c21(ACTIVE(and(active(__(mark(z0), mark(z1))), x1)), AND(mark(__(z0, z1)), x1), MARK(__(z0, z1)))
MARK(and(nil, x1)) → c21(ACTIVE(and(active(nil), x1)), AND(mark(nil), x1), MARK(nil))
MARK(and(and(z0, z1), x1)) → c21(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c21(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(isList(z0), x1)) → c21(ACTIVE(and(active(isList(z0)), x1)), AND(mark(isList(z0)), x1), MARK(isList(z0)))
MARK(and(isNeList(z0), x1)) → c21(ACTIVE(and(active(isNeList(z0)), x1)), AND(mark(isNeList(z0)), x1), MARK(isNeList(z0)))
MARK(and(isQid(z0), x1)) → c21(ACTIVE(and(active(isQid(z0)), x1)), AND(mark(isQid(z0)), x1), MARK(isQid(z0)))
MARK(and(isNePal(z0), x1)) → c21(ACTIVE(and(active(isNePal(z0)), x1)), AND(mark(isNePal(z0)), x1), MARK(isNePal(z0)))
MARK(and(isPal(z0), x1)) → c21(ACTIVE(and(active(isPal(z0)), x1)), AND(mark(isPal(z0)), x1), MARK(isPal(z0)))
MARK(and(a, x1)) → c21(ACTIVE(and(active(a), x1)), AND(mark(a), x1), MARK(a))
MARK(and(e, x1)) → c21(ACTIVE(and(active(e), x1)), AND(mark(e), x1), MARK(e))
MARK(and(i, x1)) → c21(ACTIVE(and(active(i), x1)), AND(mark(i), x1), MARK(i))
MARK(and(o, x1)) → c21(ACTIVE(and(active(o), x1)), AND(mark(o), x1), MARK(o))
MARK(and(u, x1)) → c21(ACTIVE(and(active(u), x1)), AND(mark(u), x1), MARK(u))
MARK(and(x0, x1)) → c21(AND(mark(x0), x1))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c7, c10, c12, c23, c24, c25, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c6, c8, c9, c11, c19, c21, c21

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0)) by

MARK(isQid(x0)) → c25(ISQID(x0))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)

Tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))
MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))
MARK(and(z0, z1)) → c21(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(__(z0, z1), x1)) → c21(ACTIVE(and(active(__(mark(z0), mark(z1))), x1)), AND(mark(__(z0, z1)), x1), MARK(__(z0, z1)))
MARK(and(nil, x1)) → c21(ACTIVE(and(active(nil), x1)), AND(mark(nil), x1), MARK(nil))
MARK(and(and(z0, z1), x1)) → c21(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c21(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(isList(z0), x1)) → c21(ACTIVE(and(active(isList(z0)), x1)), AND(mark(isList(z0)), x1), MARK(isList(z0)))
MARK(and(isNeList(z0), x1)) → c21(ACTIVE(and(active(isNeList(z0)), x1)), AND(mark(isNeList(z0)), x1), MARK(isNeList(z0)))
MARK(and(isQid(z0), x1)) → c21(ACTIVE(and(active(isQid(z0)), x1)), AND(mark(isQid(z0)), x1), MARK(isQid(z0)))
MARK(and(isNePal(z0), x1)) → c21(ACTIVE(and(active(isNePal(z0)), x1)), AND(mark(isNePal(z0)), x1), MARK(isNePal(z0)))
MARK(and(isPal(z0), x1)) → c21(ACTIVE(and(active(isPal(z0)), x1)), AND(mark(isPal(z0)), x1), MARK(isPal(z0)))
MARK(and(a, x1)) → c21(ACTIVE(and(active(a), x1)), AND(mark(a), x1), MARK(a))
MARK(and(e, x1)) → c21(ACTIVE(and(active(e), x1)), AND(mark(e), x1), MARK(e))
MARK(and(i, x1)) → c21(ACTIVE(and(active(i), x1)), AND(mark(i), x1), MARK(i))
MARK(and(o, x1)) → c21(ACTIVE(and(active(o), x1)), AND(mark(o), x1), MARK(o))
MARK(and(u, x1)) → c21(ACTIVE(and(active(u), x1)), AND(mark(u), x1), MARK(u))
MARK(and(x0, x1)) → c21(AND(mark(x0), x1))
MARK(isQid(x0)) → c25(ISQID(x0))

S tuples:

ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
ACTIVE(isList(__(x0, x1))) → c6(MARK(and(isList(x0), isList(x1))), ISLIST(x0), ISLIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c8(MARK(and(isList(x0), isNeList(x1))), ISLIST(x0), ISNELIST(x1))
ACTIVE(isNeList(__(x0, x1))) → c9(MARK(and(isNeList(x0), isList(x1))), ISNELIST(x0), ISLIST(x1))
ACTIVE(isNePal(__(x0, __(x1, x0)))) → c11(MARK(and(isQid(x0), isPal(x1))), ISQID(x0), ISPAL(x1))
MARK(__(z0, x1)) → c19(ACTIVE(__(z0, mark(x1))), __'(mark(z0), mark(x1)), MARK(z0), MARK(x1))
MARK(__(x0, z1)) → c19(ACTIVE(__(mark(x0), z1)), __'(mark(x0), mark(z1)), MARK(x0), MARK(z1))
MARK(__(x0, __(z0, z1))) → c19(ACTIVE(__(mark(x0), active(__(mark(z0), mark(z1))))), __'(mark(x0), mark(__(z0, z1))), MARK(x0), MARK(__(z0, z1)))
MARK(__(x0, nil)) → c19(ACTIVE(__(mark(x0), active(nil))), __'(mark(x0), mark(nil)), MARK(x0), MARK(nil))
MARK(__(x0, and(z0, z1))) → c19(ACTIVE(__(mark(x0), active(and(mark(z0), z1)))), __'(mark(x0), mark(and(z0, z1))), MARK(x0), MARK(and(z0, z1)))
MARK(__(x0, tt)) → c19(ACTIVE(__(mark(x0), active(tt))), __'(mark(x0), mark(tt)), MARK(x0), MARK(tt))
MARK(__(x0, isList(z0))) → c19(ACTIVE(__(mark(x0), active(isList(z0)))), __'(mark(x0), mark(isList(z0))), MARK(x0), MARK(isList(z0)))
MARK(__(x0, isNeList(z0))) → c19(ACTIVE(__(mark(x0), active(isNeList(z0)))), __'(mark(x0), mark(isNeList(z0))), MARK(x0), MARK(isNeList(z0)))
MARK(__(x0, isQid(z0))) → c19(ACTIVE(__(mark(x0), active(isQid(z0)))), __'(mark(x0), mark(isQid(z0))), MARK(x0), MARK(isQid(z0)))
MARK(__(x0, isNePal(z0))) → c19(ACTIVE(__(mark(x0), active(isNePal(z0)))), __'(mark(x0), mark(isNePal(z0))), MARK(x0), MARK(isNePal(z0)))
MARK(__(x0, isPal(z0))) → c19(ACTIVE(__(mark(x0), active(isPal(z0)))), __'(mark(x0), mark(isPal(z0))), MARK(x0), MARK(isPal(z0)))
MARK(__(x0, a)) → c19(ACTIVE(__(mark(x0), active(a))), __'(mark(x0), mark(a)), MARK(x0), MARK(a))
MARK(__(x0, e)) → c19(ACTIVE(__(mark(x0), active(e))), __'(mark(x0), mark(e)), MARK(x0), MARK(e))
MARK(__(x0, i)) → c19(ACTIVE(__(mark(x0), active(i))), __'(mark(x0), mark(i)), MARK(x0), MARK(i))
MARK(__(x0, o)) → c19(ACTIVE(__(mark(x0), active(o))), __'(mark(x0), mark(o)), MARK(x0), MARK(o))
MARK(__(x0, u)) → c19(ACTIVE(__(mark(x0), active(u))), __'(mark(x0), mark(u)), MARK(x0), MARK(u))
MARK(__(__(z0, z1), x1)) → c19(ACTIVE(__(active(__(mark(z0), mark(z1))), mark(x1))), __'(mark(__(z0, z1)), mark(x1)), MARK(__(z0, z1)), MARK(x1))
MARK(__(nil, x1)) → c19(ACTIVE(__(active(nil), mark(x1))), __'(mark(nil), mark(x1)), MARK(nil), MARK(x1))
MARK(__(and(z0, z1), x1)) → c19(ACTIVE(__(active(and(mark(z0), z1)), mark(x1))), __'(mark(and(z0, z1)), mark(x1)), MARK(and(z0, z1)), MARK(x1))
MARK(__(tt, x1)) → c19(ACTIVE(__(active(tt), mark(x1))), __'(mark(tt), mark(x1)), MARK(tt), MARK(x1))
MARK(__(isList(z0), x1)) → c19(ACTIVE(__(active(isList(z0)), mark(x1))), __'(mark(isList(z0)), mark(x1)), MARK(isList(z0)), MARK(x1))
MARK(__(isNeList(z0), x1)) → c19(ACTIVE(__(active(isNeList(z0)), mark(x1))), __'(mark(isNeList(z0)), mark(x1)), MARK(isNeList(z0)), MARK(x1))
MARK(__(isQid(z0), x1)) → c19(ACTIVE(__(active(isQid(z0)), mark(x1))), __'(mark(isQid(z0)), mark(x1)), MARK(isQid(z0)), MARK(x1))
MARK(__(isNePal(z0), x1)) → c19(ACTIVE(__(active(isNePal(z0)), mark(x1))), __'(mark(isNePal(z0)), mark(x1)), MARK(isNePal(z0)), MARK(x1))
MARK(__(isPal(z0), x1)) → c19(ACTIVE(__(active(isPal(z0)), mark(x1))), __'(mark(isPal(z0)), mark(x1)), MARK(isPal(z0)), MARK(x1))
MARK(__(a, x1)) → c19(ACTIVE(__(active(a), mark(x1))), __'(mark(a), mark(x1)), MARK(a), MARK(x1))
MARK(__(e, x1)) → c19(ACTIVE(__(active(e), mark(x1))), __'(mark(e), mark(x1)), MARK(e), MARK(x1))
MARK(__(i, x1)) → c19(ACTIVE(__(active(i), mark(x1))), __'(mark(i), mark(x1)), MARK(i), MARK(x1))
MARK(__(o, x1)) → c19(ACTIVE(__(active(o), mark(x1))), __'(mark(o), mark(x1)), MARK(o), MARK(x1))
MARK(__(u, x1)) → c19(ACTIVE(__(active(u), mark(x1))), __'(mark(u), mark(x1)), MARK(u), MARK(x1))
MARK(and(z0, z1)) → c21(ACTIVE(and(z0, z1)), AND(mark(z0), z1), MARK(z0))
MARK(and(__(z0, z1), x1)) → c21(ACTIVE(and(active(__(mark(z0), mark(z1))), x1)), AND(mark(__(z0, z1)), x1), MARK(__(z0, z1)))
MARK(and(nil, x1)) → c21(ACTIVE(and(active(nil), x1)), AND(mark(nil), x1), MARK(nil))
MARK(and(and(z0, z1), x1)) → c21(ACTIVE(and(active(and(mark(z0), z1)), x1)), AND(mark(and(z0, z1)), x1), MARK(and(z0, z1)))
MARK(and(tt, x1)) → c21(ACTIVE(and(active(tt), x1)), AND(mark(tt), x1), MARK(tt))
MARK(and(isList(z0), x1)) → c21(ACTIVE(and(active(isList(z0)), x1)), AND(mark(isList(z0)), x1), MARK(isList(z0)))
MARK(and(isNeList(z0), x1)) → c21(ACTIVE(and(active(isNeList(z0)), x1)), AND(mark(isNeList(z0)), x1), MARK(isNeList(z0)))
MARK(and(isQid(z0), x1)) → c21(ACTIVE(and(active(isQid(z0)), x1)), AND(mark(isQid(z0)), x1), MARK(isQid(z0)))
MARK(and(isNePal(z0), x1)) → c21(ACTIVE(and(active(isNePal(z0)), x1)), AND(mark(isNePal(z0)), x1), MARK(isNePal(z0)))
MARK(and(isPal(z0), x1)) → c21(ACTIVE(and(active(isPal(z0)), x1)), AND(mark(isPal(z0)), x1), MARK(isPal(z0)))
MARK(and(a, x1)) → c21(ACTIVE(and(active(a), x1)), AND(mark(a), x1), MARK(a))
MARK(and(e, x1)) → c21(ACTIVE(and(active(e), x1)), AND(mark(e), x1), MARK(e))
MARK(and(i, x1)) → c21(ACTIVE(and(active(i), x1)), AND(mark(i), x1), MARK(i))
MARK(and(o, x1)) → c21(ACTIVE(and(active(o), x1)), AND(mark(o), x1), MARK(o))
MARK(and(u, x1)) → c21(ACTIVE(and(active(u), x1)), AND(mark(u), x1), MARK(u))
MARK(and(x0, x1)) → c21(AND(mark(x0), x1))
MARK(isQid(x0)) → c25(ISQID(x0))

K tuples:none
Defined Rule Symbols:

active, mark, __, and, isList, isNeList, isQid, isNePal, isPal

Defined Pair Symbols:

ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL

Compound Symbols:

c, c1, c2, c3, c4, c7, c10, c12, c23, c24, c26, c27, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c6, c8, c9, c11, c19, c21, c21, c25

(21) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match(-raise)-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4, 5, 6, 7, 8, 9]
transitions:
active0(0) → 1
mark0(0) → 2
__0(0, 0) → 3
and0(0, 0) → 4
isList0(0) → 5
isNeList0(0) → 6
isQid0(0) → 7
isNePal0(0) → 8
isPal0(0) → 9
nil1() → 10
active1(10) → 2
nil1() → 0
tt1() → 11
active1(11) → 2
tt1() → 0
a1() → 12
active1(12) → 2
a1() → 0
e1() → 13
active1(13) → 2
e1() → 0
i1() → 14
active1(14) → 2
i1() → 0
o1() → 15
active1(15) → 2
o1() → 0
u1() → 16
active1(16) → 2
u1() → 0
nil1() → 17
tt1() → 18
a1() → 19
e1() → 20
i1() → 21
o1() → 22
u1() → 23
active0(17) → 1
active0(18) → 1
active0(19) → 1
active0(20) → 1
active0(21) → 1
active0(22) → 1
active0(23) → 1
mark0(17) → 2
mark0(18) → 2
mark0(19) → 2
mark0(20) → 2
mark0(21) → 2
mark0(22) → 2
mark0(23) → 2
__0(17, 0) → 3
__0(0, 17) → 3
__0(18, 0) → 3
__0(0, 18) → 3
__0(19, 0) → 3
__0(0, 19) → 3
__0(20, 0) → 3
__0(0, 20) → 3
__0(21, 0) → 3
__0(0, 21) → 3
__0(22, 0) → 3
__0(0, 22) → 3
__0(23, 0) → 3
__0(0, 23) → 3
__0(17, 17) → 3
__0(17, 18) → 3
__0(17, 19) → 3
__0(17, 20) → 3
__0(17, 21) → 3
__0(17, 22) → 3
__0(17, 23) → 3
__0(18, 17) → 3
__0(19, 17) → 3
__0(20, 17) → 3
__0(21, 17) → 3
__0(22, 17) → 3
__0(23, 17) → 3
__0(18, 18) → 3
__0(18, 19) → 3
__0(18, 20) → 3
__0(18, 21) → 3
__0(18, 22) → 3
__0(18, 23) → 3
__0(19, 18) → 3
__0(20, 18) → 3
__0(21, 18) → 3
__0(22, 18) → 3
__0(23, 18) → 3
__0(19, 19) → 3
__0(19, 20) → 3
__0(19, 21) → 3
__0(19, 22) → 3
__0(19, 23) → 3
__0(20, 19) → 3
__0(21, 19) → 3
__0(22, 19) → 3
__0(23, 19) → 3
__0(20, 20) → 3
__0(20, 21) → 3
__0(20, 22) → 3
__0(20, 23) → 3
__0(21, 20) → 3
__0(22, 20) → 3
__0(23, 20) → 3
__0(21, 21) → 3
__0(21, 22) → 3
__0(21, 23) → 3
__0(22, 21) → 3
__0(23, 21) → 3
__0(22, 22) → 3
__0(22, 23) → 3
__0(23, 22) → 3
__0(23, 23) → 3
and0(17, 0) → 4
and0(0, 17) → 4
and0(18, 0) → 4
and0(0, 18) → 4
and0(19, 0) → 4
and0(0, 19) → 4
and0(20, 0) → 4
and0(0, 20) → 4
and0(21, 0) → 4
and0(0, 21) → 4
and0(22, 0) → 4
and0(0, 22) → 4
and0(23, 0) → 4
and0(0, 23) → 4
and0(17, 17) → 4
and0(17, 18) → 4
and0(17, 19) → 4
and0(17, 20) → 4
and0(17, 21) → 4
and0(17, 22) → 4
and0(17, 23) → 4
and0(18, 17) → 4
and0(19, 17) → 4
and0(20, 17) → 4
and0(21, 17) → 4
and0(22, 17) → 4
and0(23, 17) → 4
and0(18, 18) → 4
and0(18, 19) → 4
and0(18, 20) → 4
and0(18, 21) → 4
and0(18, 22) → 4
and0(18, 23) → 4
and0(19, 18) → 4
and0(20, 18) → 4
and0(21, 18) → 4
and0(22, 18) → 4
and0(23, 18) → 4
and0(19, 19) → 4
and0(19, 20) → 4
and0(19, 21) → 4
and0(19, 22) → 4
and0(19, 23) → 4
and0(20, 19) → 4
and0(21, 19) → 4
and0(22, 19) → 4
and0(23, 19) → 4
and0(20, 20) → 4
and0(20, 21) → 4
and0(20, 22) → 4
and0(20, 23) → 4
and0(21, 20) → 4
and0(22, 20) → 4
and0(23, 20) → 4
and0(21, 21) → 4
and0(21, 22) → 4
and0(21, 23) → 4
and0(22, 21) → 4
and0(23, 21) → 4
and0(22, 22) → 4
and0(22, 23) → 4
and0(23, 22) → 4
and0(23, 23) → 4
isList0(17) → 5
isList0(18) → 5
isList0(19) → 5
isList0(20) → 5
isList0(21) → 5
isList0(22) → 5
isList0(23) → 5
isNeList0(17) → 6
isNeList0(18) → 6
isNeList0(19) → 6
isNeList0(20) → 6
isNeList0(21) → 6
isNeList0(22) → 6
isNeList0(23) → 6
isQid0(17) → 7
isQid0(18) → 7
isQid0(19) → 7
isQid0(20) → 7
isQid0(21) → 7
isQid0(22) → 7
isQid0(23) → 7
isNePal0(17) → 8
isNePal0(18) → 8
isNePal0(19) → 8
isNePal0(20) → 8
isNePal0(21) → 8
isNePal0(22) → 8
isNePal0(23) → 8
isPal0(17) → 9
isPal0(18) → 9
isPal0(19) → 9
isPal0(20) → 9
isPal0(21) → 9
isPal0(22) → 9
isPal0(23) → 9
active1(17) → 2
active1(18) → 2
active1(19) → 2
active1(20) → 2
active1(21) → 2
active1(22) → 2
active1(23) → 2
active1(17) → 1
active1(18) → 1
active1(19) → 1
active1(20) → 1
active1(21) → 1
active1(22) → 1
active1(23) → 1

(22) BOUNDS(O(1), O(n^1))